T:Type, B:(T(Top+Top)), L:T List.
concat(map(x.Case B(x) of inl(a)  [a] ; inr(a)  nil;L))
~
mapfilter(x.outl(B(x));x.isl(B(x));L) 

latex

Definitions	t  T, x:A. B(x), Top, mapfilter(f;P;L), False, A, True, P  Q, b, b, , Prop, isl(x), P & Q, P  Q, Unit, x(s), concat(ll)
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, isl wf, bool wf, bnot wf, assert wf, true wf, not wf, false wf, top wf